/*
 * EscMissesBugInterprocedural.java
 *
 * Copyright 2007 Christoph Csallner and Yannis Smaragdakis.
 */
package edu.gatech.cc.cnc.examples;

/**
 * The missed bug is caused by ESC/Java currently assuming that a method
 * does not have any side-effects if not specified otherwise
 * (no modifies clasuse).
 * This is a known ESC/Java issue and may be changed in future versions:
 * http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/docs/Escjava2-ImplementationNotes.pdf
 * 
 * @author csallner@gatech.edu (Christoph Csallner)
 */
public class EscMissesBugInterprocedural {

  /**
   * ESC/Java produces the same bug warnings for any initial field values.
   */
  private int field = 5;

  private void setField(int i) {
    field = i;
  }

  /**
   * ESC/Java generally assumes arbitrary field values.
   * So ESC/Java warns about a division by zero here.
   * This is a false bug warning, since looking at all methods of this class
   * tells us that field==5 holds before and after each public method.
   */
  public int readField() {
    return 10/field;
  }
  
  /**
   * ESC/Java can prove that division is never by zero.
   * So ESC/Java does not warn about a division by zero here.
   */
  public int setReadField() {
    field = 5;
    return 10/field;
  }  
  
  /**
   * ESC/Java does not assume arbitrary side-effects of method calls on fields.
   * So ESC/Java does not warn about a division by zero here.
   * ESC/Java therefore misses this division by zero.
   */
  public int setCallReadField() {
    field = 5;
    setField(0);
    int res = 10/field;
    field = 5;
    return res;
  }
}
